M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:(M.ds(x)). M.ef(k,x,s,v,w)   

latex

Definitions	MsgA, M.state, M.da(a), M.ef(k,x,s,v,w), M.ds(x), z != f(x)  P(a;z), b, x  dom(f), , s = t, suptype(S; T), f(a), f(x), P  Q, product-deq(A;B;a;b), a:A fp B(a), t.1, x:A  B(x), t.2, <a, b>, , KindDeq, State(ds), Knd, Valtype(da;k), S  T, x:AB(x), x. t(x), x.A(x), Top, f(x)?z, Void, Type, x:A. B(x), Id, IdDeq, t  T
Lemmas	id-deq wf, Id wf, fpf-cap-void-subtype, fpf-cap wf, Knd wf, ma-state wf, top wf, Kind-deq wf, rationals wf, pi2 wf, pi1 wf, ma-valtype wf, fpf-trivial-subtype-top, product-deq wf, fpf-ap wf, fpf-dom wf, assert wf, msga wf